(declare-sort S0 0)

(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i4 Int)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const r15 Real)
(assert (exists ((q0 (_ BitVec 10)) (q1 Int) (q2 Int) (q3 (_ BitVec 4))) (=> (distinct q0 #b1010011000 q0 #b1010011000) (distinct 773 q2))))
(declare-const v22 Bool)
(declare-const i8 Int)
(assert (forall ((q4 (_ BitVec 9)) (q5 Int) (q6 (_ BitVec 4))) v15))
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const i9 Int)
(declare-const v26 Bool)
(declare-const _18-0 (_ BitVec 18))
(declare-const v27 Bool)
(declare-const i10 Int)
(assert (or v1))
(assert (or v3 v3 v13 (= (_ bv407 9) (_ bv407 9) (_ bv407 9) (_ bv407 9) (_ bv407 9))))
(assert (or (<= 973876.0 r2) (is_int r3) v13 v13))
(check-sat)
